package ch.epfl.lara.matcheck.ast.parser;

import ch.epfl.lara.matcheck.util.{Substitute,ShapeKeeper}

object Desugar extends ShapeKeeper {

  def apply[T<:Tree](t: T): T = (t match {
    case Program(constr,extr,objs,clss) => cast[T,Program]  (Program(constr,extr,objs.map(this(_)),clss.map(this(_))))
    case ObjectDef(name,inv,methods)    => cast[T,ObjectDef](ObjectDef(name,inv,methods.map(this(_))))
    case ClassDef(isSealed,isAbs,name,fields,superc,inv,methods) =>
      val invar = inv match {case None => inv case Some(i) => Some(this(name.getSym,i))}
      name.sym.invariant = invar
      cast[T,ClassDef] (ClassDef(isSealed,isAbs,name,fields,superc,invar,methods.map(this(name.getSym,_))))
    case _ => t
  }).setPos(t.pos)
  
  
  def apply[T<:Members](cs: ClassSymbol, m: T): T = (m match {
    case MethodDef(name,params,retTpe,Some((pre,post)),body) =>
      val precondition: Formula = this(cs,pre)
      val postcondition: Formula = this(cs,post)
      val ppc = Some((precondition,postcondition))
      name.sym.ppc = ppc
      cast[T,MethodDef] (MethodDef(name,params,retTpe,ppc,this(body)))
    case _ => m
  }).setPos(m.pos)
  
  def apply(cs: ClassSymbol, f: Formula): Formula = {
    
    def iter[T<:Formula](f: T): T = f match {
      case And(left,right)          => cast[T,And]           (And(iter(left),iter(right)))
      case Or(left,right)           => cast[T,Or]            (Or(iter(left),iter(right)))
      case Neg(f)                   => cast[T,Neg]           (Neg(iter(f)))
      case Imply(left,right)        => cast[T,Imply]         (Imply(iter(left),iter(right)))
      case Equality(left,right)        => cast[T,Equality]         (Equality(iter(left),iter(right)))
      case Forall(x,f)              => cast[T,Forall]        (Forall(x,iter(f)))
      case SubsetEq(left,right)     => cast[T,SubsetEq]      (SubsetEq(iter(left),iter(right)))
      case EqSet(left,right)        => cast[T,EqSet]         (EqSet(iter(left),iter(right)))
      case In(x,set)                => cast[T,In]            (In(iter(x),iter(set)))
      case Union(left,right)        => cast[T,Union]         (Union(iter(left),iter(right)))
      case Intersection(left,right) => cast[T,Intersection]  (Intersection(iter(left),iter(right)))
      case Eq(left,right)           => cast[T,Eq]            (Eq(iter(left),iter(right)))
      case NotEq(left,right)        => cast[T,NotEq]         (NotEq(iter(left),iter(right)))
      case Less(left,right)         => cast[T,Less]          (Less(iter(left),iter(right)))
      case LessEq(left,right)       => cast[T,LessEq]        (LessEq(iter(left),iter(right)))
      case Plus(left,right)         => cast[T,Plus]          (Plus(iter(left),iter(right)))
      case Minus(left,right)        => cast[T,Minus]         (Minus(iter(left),iter(right)))
      case Div(left,right)          => cast[T,Div]           (Div(iter(left),iter(right)))
      case Prod(left,right)         => cast[T,Prod]          (Prod(iter(left),iter(right)))
      case Mod(left,right)          => cast[T,Mod]           (Mod(iter(left),iter(right)))
      case Function(name,elems)     => cast[T,Function]      (Function(name,elems.map(iter(_))))
      case Element(x)               => f
      case Set(name)                => f
      case Tru  | EmptySet |  
           Flse | Const(_) | 
           StringLit0(_)            => f
      case d @ Deref(obj,_)     =>
           def flatten(cs: ClassSymbol, cd: CodeTerm, param: Term): Term = cd match {
             case Element(name) => 
               Function(cs.getName + "_getField_" + name, List(param))
             
             case Deref(Element(objname),field)  =>
               field match {
                 case e : Element => flatten(cs,field,param)
                   //Function(cs.getName + "_getField_" + fname, List(param))
                 
                 case Deref(Element(fname),pathfield)  =>
                   val sym = cs.lookupField(fname) match {
                     case None => 
                       Report.error(d.pos,"can't find symbol for field '"+fname+"' in class "+cs.getName)
                       null
                 
                     case Some(fs) => fs.name.getSym
                   }
                   
                 flatten(sym,pathfield,Function(cs.getName + "_getField_" + fname, List(param)))
             }
           }
           
           cast[T,Formula] (flatten(cs, d, obj))
           
    }
    iter(f)
  }
}
